(declare-fun r1 () Real)
(declare-fun v1 () Bool)
(declare-fun r0 () Real)
(declare-fun r3 () Real)
(declare-fun r4 () Real)
(declare-fun r6 () Real)
(push)
(assert false)
(check-sat)
(pop)
(assert (= true true v1 (= (* 7.1312 (+ r0 r6 r4 7.1312) r0 r3 (+ r0 r6 r4 7.1312)) r4 (- r6) 259709.0 (* r0 r3 43559.0 r6 r6) r1)))
(check-sat)
(assert false)
(check-sat)
(pop)
